Ouch. Selftests are failing because of a change to the batch-mode error reporting. Will be a few days before I clean this up. But a bin/build at level 1 works fine, should anyone want to have a gander.

This is now ready. There weren't many problems with the selftests. I haven't looked at MoscowML.

But, as I wrote above, at least two things need to be improved once this change is (I hope) accepted.

1. Type inference error messages
2. The distinction between "repl_mode" and "batch_mode", ie, whether Globals.interactive is true or false, needs to be propagated more widely. For example, the possible exceptions coming out of the "events" of Modern Syntax (Definition, Theorem, Datatype, (Co)Inductive, etc) need to be treated differently depending on which mode the system is in. Thanks to Michael's previous work, Definition is largely taken care of, but for Theorem I need to look for something named (guessing) located_prove_thm or some such.

The mode distinction and its treatment is straightforward (Michael's code):

fun render_exn srcfn e =
    if !Globals.interactive then
       raise e
    else
      (output_ERR (exn_to_string e);
       raise BATCH_ERR srcfn)

Basically BATCH_ERR is used to avoid being caught by HOL_ERR handlers, which result in tedious replication of messages. It's used in situations where an excellent top-level error message has already been printed, so any further messaging is just annoying.

... Having looked at it a bit more, I wonder whether the invocation of render_exn on Modern Syntax elements should be done in the SML definitions ultimately invoked, or when HolParser runs.

Per @ordinarymath 's original idea, HOL_ERROR (the argument to HOL_ERR) now constructs a stack of origins + message. This allows wrap_exn to be more efficient and feels cleaner. Still to do: making sure that Modern Syntax displays HOL_ERRs nicely in both interactive and batch mode, making the change work in MoscowML, and checking the impact on CakeML.

I'll investigate into the impact on CakeML later this week

OK, have now built on MoscowML. There were a few files that seem to get built for mosml but not PolyML (some in HolQbf and patriciaLib.sml).

I also seem to have found the answer to the highly vexing question "why doesn't the REPL invoke the installed prettyprinter for hol_error when printing the value HOL_ERR empty_hol_error"? The answer seems to be that Feedback is opaquely constrained by its signature via :>. Nevermind that the datatype declaration for hol_error is made explicit in Feedback.sig. Some obscure (to me) aspect of signature curtailment meant the that REPL prettyprinter couldn't invoke the installed prettyprinter for hol_error and defaulted to printing the representation.

Time to move this over to develop. There is a bit more tidying up to do, but the main stuff is done.

1. Revision to type-checking error messages. The current ones are terrible because (a) they get duplicated in the REPL and (b) they're horribly verbose. So they have been made more akin to those coming out of the PolyML typechecker. The code is simpler too. However, the term parser gets invoked in all kind of ways, so there may yet be problems. In fact, I think I have one difficulty already (see next point).
2. Ongoing effort to get Modern Syntax failures (and failures in other, lower-level, theory "events") to get displayed through Feedback.render_exn which acts differently depending on whether in Globals.interactive mode or not. Two things : (a) I don't seem to be picking up location information from Modern Syntax as I'd hoped, and (b) The revision in (a) got rid of intermediate printing in the typechecker and so now something like

Theorem foo:                                                                                                                                                                                      
  1 = T                                                                                                                                                                                           
Proof
  NO_TAC
QED

in the REPL, gives the following:

Exception-
   HOL_ERR
     (at Q.store_thm_at:
        at Parse.typed_parse_in_context: No consistent parse) raised

while just invoking the parser on the badly typed formula in the REPL actually shows the problem

> ``1 = T``;
Exception-
   HOL_ERR
     (at Preterm.type-analysis: at line 101, character 6:

Type error in function application.
  Function: $= 1 :num -> bool
  Argument: T :bool
  Reason: Attempt to unify different type operators: num$num and min$bool
)
   raised

The problem seems to be in parse_in_context but I haven't yet tracked it down or fixed it.

Setting this back to being a draft PR until the parse_in_context problem gets sorted

The parse_in_context problem is partly solved, in that things like Theorem error out in an informative way now. But parse_in_context is (I think) used to help backtracking in "thm_tacticals" and there's at least one selftest that therefore fails because of the change in error reporting. Commenting that one out for now in the interest of getting this over to develop.